the_es:event_system{i:l}, e,e':es-E(the_es).
((es-first(the_es; e')))
 (es-le(the_es; e; es-pred(the_es; e'))  es-locl(the_es; e; e')) 

latex

Definitions	t  T, P  Q, x:A. B(x), es-pred(es; e), es-E(es), prop{i:l}, es-locl(es; e; e'), P  Q, guard(T), es-le(es; e; e'), es-first(es; e), b, A, P  Q, P  Q, P  Q, event_system{i:l}
Lemmas	event system wf, iff functionality wrt iff, es-locl-iff, es-le wf, not wf, assert wf, es-first wf, es-locl wf, es-E wf, es-pred wf